(set-logic QF_BV)
(set-info :source |
    Sequential equivalence checking.
    Calypto Design Systems, Inc. <www.calypto.com>
  |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun P_2 () (_ BitVec 9))
(declare-fun P_3 () (_ BitVec 9))
(declare-fun P_4 () (_ BitVec 9))
(declare-fun P_5 () (_ BitVec 9))
(declare-fun P_6 () (_ BitVec 9))
(declare-fun P_7 () (_ BitVec 9))
(declare-fun P_8 () (_ BitVec 9))
(declare-fun P_9 () (_ BitVec 9))
(declare-fun P_10 () (_ BitVec 9))
(declare-fun P_11 () (_ BitVec 9))
(declare-fun P_12 () (_ BitVec 9))
(declare-fun P_13 () (_ BitVec 9))
(declare-fun P_14 () (_ BitVec 9))
(declare-fun P_15 () (_ BitVec 9))
(declare-fun P_16 () (_ BitVec 9))
(declare-fun P_17 () (_ BitVec 9))
(declare-fun P_18 () (_ BitVec 9))
(declare-fun P_19 () (_ BitVec 9))
(declare-fun P_20 () (_ BitVec 9))
(declare-fun P_21 () (_ BitVec 9))
(declare-fun P_22 () (_ BitVec 9))
(declare-fun P_23 () (_ BitVec 9))
(declare-fun P_24 () (_ BitVec 9))
(declare-fun P_25 () (_ BitVec 9))
(declare-fun P_26 () (_ BitVec 9))
(declare-fun P_27 () (_ BitVec 9))
(declare-fun P_28 () (_ BitVec 9))
(declare-fun P_29 () (_ BitVec 9))
(declare-fun P_30 () (_ BitVec 9))
(declare-fun P_31 () (_ BitVec 9))
(declare-fun P_32 () (_ BitVec 9))
(declare-fun P_33 () (_ BitVec 9))
(declare-fun P_34 () (_ BitVec 9))
(declare-fun P_35 () (_ BitVec 9))
(declare-fun P_36 () (_ BitVec 9))
(declare-fun P_37 () (_ BitVec 9))
(declare-fun P_38 () (_ BitVec 9))
(declare-fun P_39 () (_ BitVec 9))
(declare-fun P_40 () (_ BitVec 9))
(declare-fun P_41 () (_ BitVec 9))
(declare-fun P_42 () (_ BitVec 9))
(declare-fun P_43 () (_ BitVec 9))
(declare-fun P_44 () (_ BitVec 9))
(declare-fun P_45 () (_ BitVec 9))
(declare-fun P_46 () (_ BitVec 9))
(declare-fun P_47 () (_ BitVec 9))
(declare-fun P_48 () (_ BitVec 9))
(declare-fun P_49 () (_ BitVec 9))
(declare-fun P_50 () (_ BitVec 9))
(declare-fun P_51 () (_ BitVec 9))
(declare-fun P_52 () (_ BitVec 9))
(declare-fun P_53 () (_ BitVec 9))
(declare-fun P_54 () (_ BitVec 9))
(declare-fun P_55 () (_ BitVec 9))
(declare-fun P_56 () (_ BitVec 9))
(declare-fun P_57 () (_ BitVec 9))
(declare-fun P_58 () (_ BitVec 9))
(declare-fun P_59 () (_ BitVec 9))
(declare-fun P_60 () (_ BitVec 9))
(declare-fun P_61 () (_ BitVec 9))
(declare-fun P_62 () (_ BitVec 9))
(declare-fun P_63 () (_ BitVec 9))
(declare-fun P_64 () (_ BitVec 9))
(declare-fun P_65 () (_ BitVec 9))
(declare-fun P_66 () (_ BitVec 15))
(assert (let ((?v_0 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_4) ((_ sign_extend 1) P_5)))) (?v_1 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_6) ((_ sign_extend 1) P_7))))) (let ((?v_2 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_2) ((_ sign_extend 1) P_3)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_0 ?v_1))))))) (let ((?v_3 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_2) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_8) ((_ sign_extend 1) P_9)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_0 ?v_1)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_2) (_ bv2147483083 31)))))) (let ((?v_51 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_3) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_3) (_ bv11 32))) (bvlshr ?v_3 (_ bv11 32)))))) (?v_4 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_12) ((_ sign_extend 1) P_13)))) (?v_5 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_14) ((_ sign_extend 1) P_15))))) (let ((?v_6 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_10) ((_ sign_extend 1) P_11)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvadd ?v_4 ?v_5)) (_ bv181 19)))))) (let ((?v_7 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_6) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_16) ((_ sign_extend 1) P_17)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvsub ?v_4 ?v_5))))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_6) (_ bv2147483083 31)))))) (let ((?v_52 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_7) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_7) (_ bv11 32))) (bvlshr ?v_7 (_ bv11 32))))))) (let ((?v_39 ((_ sign_extend 1) (bvadd ?v_51 ?v_52))) (?v_8 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_20) ((_ sign_extend 1) P_21)))) (?v_9 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_22) ((_ sign_extend 1) P_23))))) (let ((?v_10 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_18) ((_ sign_extend 1) P_19)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_8 ?v_9))))))) (let ((?v_11 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_10) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_24) ((_ sign_extend 1) P_25)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_8 ?v_9)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_10) (_ bv2147483083 31)))))) (let ((?v_43 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_11) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_11) (_ bv11 32))) (bvlshr ?v_11 (_ bv11 32)))))) (?v_12 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_28) ((_ sign_extend 1) P_29)))) (?v_13 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_30) ((_ sign_extend 1) P_31))))) (let ((?v_14 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_26) ((_ sign_extend 1) P_27)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_12 ?v_13))))))) (let ((?v_15 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_14) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_32) ((_ sign_extend 1) P_33)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_12 ?v_13)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_14) (_ bv2147483083 31)))))) (let ((?v_44 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_15) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_15) (_ bv11 32))) (bvlshr ?v_15 (_ bv11 32))))))) (let ((?v_40 ((_ sign_extend 1) (bvadd ?v_43 ?v_44)))) (let ((?v_35 ((_ sign_extend 1) (bvadd ?v_39 ?v_40))) (?v_16 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_36) ((_ sign_extend 1) P_37)))) (?v_17 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_38) ((_ sign_extend 1) P_39))))) (let ((?v_18 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_34) ((_ sign_extend 1) P_35)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_16 ?v_17))))))) (let ((?v_19 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_18) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_40) ((_ sign_extend 1) P_41)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_16 ?v_17)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_18) (_ bv2147483083 31)))))) (let ((?v_46 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_19) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_19) (_ bv11 32))) (bvlshr ?v_19 (_ bv11 32)))))) (?v_20 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_44) ((_ sign_extend 1) P_45)))) (?v_21 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_46) ((_ sign_extend 1) P_47))))) (let ((?v_22 (bvsub ((_ sign_extend 2) (bvshl ((_ sign_extend 8) (bvsub ((_ sign_extend 1) P_42) ((_ sign_extend 1) P_43))) (_ bv8 18))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvadd ?v_20 ?v_21)) (_ bv181 19)))))) (let ((?v_23 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_22) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (bvshl ((_ sign_extend 8) (bvsub ((_ sign_extend 1) P_48) ((_ sign_extend 1) P_49))) (_ bv8 18))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_20 ?v_21)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_22) (_ bv2147483083 31)))))) (let ((?v_47 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_23) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_23) (_ bv11 32))) (bvlshr ?v_23 (_ bv11 32))))))) (let ((?v_37 ((_ sign_extend 1) (bvadd ?v_46 ?v_47))) (?v_24 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_52) ((_ sign_extend 1) P_53)))) (?v_25 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_54) ((_ sign_extend 1) P_55))))) (let ((?v_26 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_50) ((_ sign_extend 1) P_51)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_24 ?v_25))))))) (let ((?v_27 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_26) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_56) ((_ sign_extend 1) P_57)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_24 ?v_25)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_26) (_ bv2147483083 31)))))) (let ((?v_48 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_27) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_27) (_ bv11 32))) (bvlshr ?v_27 (_ bv11 32)))))) (?v_28 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_60) ((_ sign_extend 1) P_61)))) (?v_29 ((_ sign_extend 1) (bvsub ((_ sign_extend 1) P_62) ((_ sign_extend 1) P_63))))) (let ((?v_30 (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_58) ((_ sign_extend 1) P_59)) (_ bv0 8))) ((_ sign_extend 1) (bvmul (_ bv181 19) ((_ sign_extend 8) (bvadd ?v_28 ?v_29))))))) (let ((?v_31 (bvadd (bvmul (_ bv1703 32) ((_ sign_extend 11) (bvadd ((_ sign_extend 1) ?v_30) ((_ sign_extend 1) (bvsub ((_ sign_extend 2) (concat (bvsub ((_ sign_extend 1) P_64) ((_ sign_extend 1) P_65)) (_ bv0 8))) ((_ sign_extend 1) (bvmul ((_ sign_extend 8) (bvsub ?v_28 ?v_29)) (_ bv181 19)))))))) ((_ sign_extend 1) (bvmul ((_ sign_extend 11) ?v_30) (_ bv2147483083 31)))))) (let ((?v_49 ((_ sign_extend 1) ((_ extract 20 0) (ite (ite (= ((_ extract 31 31) ?v_31) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_31) (_ bv11 32))) (bvlshr ?v_31 (_ bv11 32))))))) (let ((?v_38 ((_ sign_extend 1) (bvadd ?v_48 ?v_49)))) (let ((?v_36 ((_ sign_extend 1) (bvadd ?v_37 ?v_38)))) (let ((?v_34 ((_ sign_extend 8) (bvadd ?v_35 ?v_36)))) (let ((?v_32 (bvmul ?v_34 (_ bv181 32)))) (let ((?v_33 ((_ extract 13 0) (ite (ite (= ((_ extract 31 31) ?v_32) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_32) (_ bv18 32))) (bvlshr ?v_32 (_ bv18 32))))) (?v_53 (bvsub ?v_51 ?v_52))) (let ((?v_61 ((_ sign_extend 2) ((_ extract 20 0) (ite (ite (= ((_ extract 21 21) ?v_53) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_53) (_ bv1 22))) (bvlshr ?v_53 (_ bv1 22)))))) (?v_54 ((_ sign_extend 1) (bvsub ?v_46 ?v_47))) (?v_55 ((_ sign_extend 1) (bvsub ?v_48 ?v_49)))) (let ((?v_56 (bvmul ((_ sign_extend 8) (bvadd ?v_54 ?v_55)) (_ bv181 31)))) (let ((?v_62 ((_ sign_extend 1) ((_ extract 21 0) (ite (ite (= ((_ extract 30 30) ?v_56) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_56) (_ bv9 31))) (bvlshr ?v_56 (_ bv9 31))))))) (let ((?v_63 ((_ sign_extend 9) (bvsub ?v_61 ?v_62))) (?v_45 (bvsub ?v_43 ?v_44))) (let ((?v_59 ((_ sign_extend 2) ((_ extract 20 0) (ite (ite (= ((_ extract 21 21) ?v_45) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_45) (_ bv1 22))) (bvlshr ?v_45 (_ bv1 22)))))) (?v_50 (bvmul ((_ sign_extend 8) (bvsub ?v_54 ?v_55)) (_ bv181 31)))) (let ((?v_60 ((_ sign_extend 1) ((_ extract 21 0) (ite (ite (= ((_ extract 30 30) ?v_50) (_ bv0 1)) false true) (bvnot (bvlshr (bvnot ?v_50) (_ bv9 31))) (bvlshr ?v_50 (_ bv9 31))))))) (let ((?v_64 ((_ sign_extend 9) (bvsub ?v_59 ?v_60))) (?v_57 ((_ sign_extend 9) (bvadd ?v_61 ?v_62))) (?v_58 ((_ sign_extend 9) (bvadd ?v_59 ?v_60))) (?v_41 (bvsub ?v_39 ?v_40)) (?v_42 (bvsub ?v_37 ?v_38)) (?v_65 ((_ sign_extend 1) ?v_33))) (let ((?v_67 (bvneg ?v_65)) (?v_66 (= (_ bv1 1) (ite (bvslt ?v_33 (_ bv0 14)) (_ bv1 1) (_ bv0 1))))) (not (= (ite ?v_66 ?v_67 (ite (= (_ bv1 1) (ite (= ((_ extract 13 13) ((_ extract 101 88) (concat (concat (concat (concat (concat (concat (concat ((_ extract 31 18) (bvmul (_ bv181 32) ?v_34)) ((_ extract 31 18) (bvmul (_ bv181 32) ((_ sign_extend 8) (bvsub ?v_35 ?v_36))))) ((_ extract 31 19) (bvadd ((_ sign_extend 1) (bvmul (_ bv196 31) ((_ sign_extend 8) ?v_42))) (bvmul (_ bv473 32) ((_ sign_extend 9) ?v_41))))) ((_ extract 31 19) (bvsub ((_ sign_extend 1) (bvmul ((_ sign_extend 8) ?v_41) (_ bv196 31))) (bvmul ((_ sign_extend 9) ?v_42) (_ bv473 32))))) ((_ extract 31 20) (bvadd (bvmul ?v_58 (_ bv400 32)) (bvmul ?v_57 (_ bv2009 32))))) ((_ extract 31 20) (bvsub (bvmul ?v_57 (_ bv400 32)) (bvmul ?v_58 (_ bv2009 32))))) ((_ extract 31 20) (bvadd (bvmul ?v_64 (_ bv1703 32)) (bvmul ?v_63 (_ bv1138 32))))) ((_ extract 31 20) (bvsub (bvmul (_ bv1703 32) ?v_63) (bvmul (_ bv1138 32) ?v_64)))))) (_ bv0 1)) (_ bv1 1) (_ bv0 1))) ?v_65 P_66)) (ite ?v_66 ?v_67 ?v_65))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
